Untitled Document

ELG 7187C --- Winter 2012 --- Assignment 2 --- Reachability Analysis

behaviors

The figure above shows the behavior of three LTSs A, B and C that communicate with one another by rendezvous for the interactions a, b, e and f, while x and y are independent, as indicated in the architecture diagram (d) below: Please consider the composition of these three machines and indicate its behavior (in the form of a single LTS), that means, do a reachability analysis (do you detect any design error ? ). If you find a problem with the design, please suggest a modification of the defined behavior for the machines in order to resolve the identified problem. Please explain !

(a) Please solve this problem by hand.
(b) Please use the LTSA tool to solve this problem. See pointers about LTSA (including a short introduction to the syntax of specifications). A number of examples can be found here (mainly for course SEG-2106); you may look at the example CoffeeMachine (which was also explained in the course notes of ELG-7187C). Some more examples are given in Lab2 for course SEG-2106.
(c) In the global behavior of this system, is the number of executions of the interactions x related to the number of executions of the interactions y ? - Explain!
(d) By adding an integer parameter to the interactions x and y, and adding a global integer variable, could one model the transfer of integer values from the left interface of the architecture (d) to the right interface of the architecture ? - And how could that be modelled ? (Hint: consider that the parameter of an interaction may be assigned to the variable during the transition, or the value of the variable may be used to determine the parameter of an interaction.) - Explain!
(e) Could one model the same data transfer without a global variable, but using several local variables, one for each LTS in the architecture ? - Which other interactions would require an integer parameter for this purpose ? - Explain!

architectures

Now we assume that the transition diagrams shown above define the behavior of three IOAs A, B and C where the interactions now are inputs or outputs as indicated in the architecture diagram (e). Please consider the composition of these three machines and indicate their joint behavior (in the form of a single state machine), that means, do a reachability analysis (do you detect any design error ? ). If you find a problem with the design, please suggest a modification of the defined behavior for the machines in order to resolve the identified problem. Please explain !

(a) Please solve this problem by hand. - Do you make any assumptions about the environment of the three IOAs ? - Explain!
(b) Please, look at the LTSA example "IOA example". It shows how one can use the LTSA tool (which was built for analysing LTS systems) to analyse IOA compositions. You may use this approach to deal with point (a).
(c) Assume that the environment at the right interface of the architecture contains a component that receives the y interactions. Suppose that this component has two states: ready and busy. In the ready state it has a transition for receiving a y interaction which leads to the busy state. In the busy state, it has no transition to receive a y interaction, but there is a spontaneous transition going from the busy state to the ready state. With the behavior specified for C, there may be a non-specified reception of y in the busy state of the component in the environment. Please modify the behavior of C and revise the behavior of the environment component in such a way that a non-specified reception is avoided (but keeping the busy state in which no y can be received). Explain your design.

Now consider only the machines A, and B with inputs and outputs (as under point (2)), but assume that they communicate asynchronously, that is an output is first put into a queue before it is received by the other side (that is, assume that we have communicating finite state machines). Please consider the composition of these two machines and indicate their behavior (in the form of a single transition diagram), that means, do a reachability analysis (do you detect any design error ? ) . If you find a problem with the design, please suggest a modification of the defined behavior for the machines in order to resolve the identified problem. If the reachable queue length is not bounded you may not be able to perform a complete reachability analysis. Please explain !